Let ℒ and ? be propositional languages over Basic Propositional Calculus, and ℳ = ℒ∩?. Weprove two different but interrelated interpolation theorems. First, suppose that Π is a sequent theory over ℒ, and Σ∪ {C⇒C′} is a set of sequents over ?, such that Π,Σ⊢C⇒C′. Then there is a sequent theory Φ over ℳ such that Π⊢Φ and Φ, Σ⊢C⇒C′. Second, let A be a formula over ℒ, and C 1, C 2 be formulas over ?, such that A∧C 1⊢C (...) 2. Then there exists a formula B over ℳ such that A⊢B and B∧C 1⊢C 2. (shrink)

In "Intuitionistic validity in -normal Kripke structures," Buss asked whether every intuitionistic theory is, for some classical theory , that of all -normal Kripke structures for which he gave an r.e. axiomatization. In the language of arithmetic and denote PA plus Open Induction or Open LNP, and are their intuitionistic deductive closures. We show is recursively axiomatizable and , while . If proves PEM but not totality of a classically provably total Diophantine function of , then and so . A (...) result due to Wehmeier then implies . We prove is not -conservative over . If , then is not closed under MR or Friedman's translation, so range (). Both and are closed under the negative translation. (shrink)

We give a counterexample to the claim that every provably total function of Basic Arithmetic is a polynomially bounded primitive recursive function.

Over the past few years we have witnessed a sharp resurgence in feminist activism as young women have become increasingly interested in feminist ideas as a means of making sense of their lives. This resurgence in feminist practice is evidenced by the formation of myriad groups and networks across Britain and the initiation of various feminist projects and campaigns, reported regularly and widely in local and national media. This article examines the renaissance of this new feminism through the example of (...) one of the most active and publicly visible organisations, UK Feminista. It draws on ethnographic research into young women’s feminist activism, exploring the emergence of UK Feminista as part of this new wave of feminist activism in Britain. We argue that the wave metaphor has multifarious meanings and that to understand how the political practice of a small feminist organisation contributes to the amplification of this wave of feminist activism it is helpful to draw on concepts developed within social movement theory such as cycles of protest, repertoires of action and collective identities. We show how UK Feminista mobilises young women and provides resources to existing and new feminist organisations and activist groups, commenting particularly on its use of the Internet and social media as a mobilising device. We explore the role of the Internet in young women’s engagement with feminism, the forms of activism in which they take part and the importance of feminist cultural memory to the construction of a collective feminist identity. Our analysis reveals the significant part played by a small mobilising structure, UK Feminista, in the resurgence of feminist activism in the UK. (shrink)

While the speed of light has the constant value of 3 × 108 m/s in vacuum, its value diminishes in denser mediums. It is the purpose of this paper to show that as light enters regions of larger gravitational fields such as Neutron Stars and Black Holes light speed is also diminished. We consider the cases of Pulsars, Quasars, and Active Galactic Nuclei, to provide experimental proof that charged particles moving faster than the diminished speed of light in these high (...) gravity regions would radiate energy due to Cherenkov Radiation that has been detected on earth as Radio Waves and X-Rays. We show that there is no experimental evidence for Hawking Radiation since the premise of its theoretical calculation is faulty. (shrink)

The connection between the infinite nature of Quantum Cosmology and the infinite nature of God is presented here. At the beginning of the creation process, there was a single God/Void that was divided into many Gods/Voids all filled with Dark Energy consisting of photons which were responsible for creating the Multiverses made of matter, antimatter, space, time, charge, and multiple dimensions of space. The one God initially had no material existence which along with the laws of science was a creation (...) of the powers of His infinite mind. Since the process of creation started with the Dark Energy of the Voids, the Conservation of Energy Principle applied to all of them. If the Dark Energy of each Void were to be finite, then its energy would begin to decrease as Multiverses were created, and the only solution for not violating the Conservation of Energy Principle was that the Dark Energy of each of the Voids must be infinite implying that the Voids themselves must be infinite, and with infinite amount of energy be able to create an infinite number of Multiverses. According to Mathematics, all infinite numbers are not equal, some infinities are greater than other infinities. Hence of the many infinite Voids that were initially created, some Voids were greater than others. Each Void has a Supreme Leader that we refer to as God, and therefore there exist many Gods, some Gods more powerful than other Gods. (shrink)

In the context of intuitionistic analysis, we consider the set consisting of all continuous functions from [0,1] to such that =0 and =1, and the set consisting of ’s in where there exists x[0,1] such that . It is well-known that there are weak counterexamples to the intermediate value theorem, and with Brouwer’s continuity principle we have . However, there exists no satisfying answer to . We try to answer to this question by reducing it to a schema about intuitionistic (...) decidability that asserts “there exists an intuitionistically enumerable set that is not intuitionistically decidable”. We also introduce the notion of strong Specker double sequence, and prove that the existence of such a double sequence is equivalent to the existence of a function where. (shrink)

In lieu of an abstract, here is a brief excerpt of the content:104 COMMENTARY ON PROFESSOR TWEYMAN ' S 'HUME ON EVIL' Philo concludes his long and celebrated debate with Cleanthes on the problem of evil (Parts X and Xl of Hume's Dialogues) with the assertion that the "true conclusion" to be drawn from the "mixed phenomena" in the world is that "the original source" of whatever order we find in the world is "indifferent" to matters of good and evil. (...) From what Philo says immediately thereafter it is clear that by the phrase "The true conclusion is..." he does not mean 'The truth is...' but rather something like 'The conclusion best supported by the available evidence is....' (D 212) Now according to both Nelson Pike and Stanley Tweyman, the claim made by Philo in these passages involves him in a shift or departure from the procedure he adopted in earlier dialogues when he examined the design argument set forth by Cleanthes. It is claimed that whereas in the earlier dialogues Philo emphatically professed a sceptical outlook — "the view requiring that one embrace no metaphysical position of one's own" (to quote Nelson Pike ) — in the quoted passage he seems to abandon this scepticism in favor of embracing what amounts to being a metaphysical position in natural theology. Pike thinks that this alleged shift is only an apparent one, that the central import of these passages is sceptical rather than metaphysical, and that here, as elsewhere in the earlier dialogues, Philo's sole purpose in offering a more plausible counter-hypothesis is to show that Cleanthes' hypothesis is false. Tweyman, on the other hand, argues that the shift is a very real one and that Hume does indeed "intend Philo's conclusion in Part XI to be a truth in natural theology [.]... Philo is 105 not arguing as a sceptic; rather he is employing the hypothetico-deductive method for testing Cleanthes' 2 hypothesis. " Let me say at once that I agree with Tweyman, as against Pike, that in these passages Philo does claim to put forward a truth Jji natural theology, and I also agree with just about everything that Tweyman says in his paper concerning the proper interpretation of Philo's views in Parts X and XI leading up to this conclusion. I follow the lead of those scholars who, at least since Kemp Smith, have argued that Philo's whole purpose in demonstrating such "truths" is to discredit natural theology in the eyes of a true Christian believer by dramatizing the enormous gulf between the very attenuated form of theism ("diaphonous deism" one scholar calls it), which is the most one can hope to get out of Cleanthes' experimental approach to religion, and the claim of Christian theism to which Cleanthes aspires. But I do not accept the view that Philo's claim in these dialogues represents any sort of sudden departure (and certainly not a "fundamental methodological difference") from his critical stance against the design argument in earlier dialogues. What I hope to show below is that not only does this view distort what Philo does in the earlier dialogues, but it also distracts our attention from the true nature of Hume's achievement in Parts X and XI of the Dialogues. (Incidentally, I will assume throughout the sequel that Kemp Smith's identification of Hume with Philo is essentially correct. ) It would indeed be extremely paradoxical, in the face of Philo's famous (or notorious) peroration at the end of Part VIII proclaiming the "complete triumph of the sceptic" in regard to "all religious 106 systems," to raise any doubts about Philo's acceptance of the sceptical import of his own earlier arguments. But this still leaves unsettled the question as to what sort of scepticism it is whose triumph Philo proclaims at this point and whether it is inconsistent with the conclusion he reaches at the end of his discussion of evil. One would have hoped that at this late stage in the scholarship on the Dialogues, if there is one issue on which all of us could agree it is that Philo at no time in the Dialogues takes the (easy) Pyrrhonian line against Cleanthes' "hypothesis of experimental theism." I mention this because at several places... (shrink)

The author sides with the linguistic philosophers in that to analyse 'moral reasoning' is to provide a conceptual description of a prescriptive or normative area of language. He considers the question of why we should adopt a "moral point of view" in terms of toulmin (who thinks it is a meaningless question) and baier and nelson (who think it is legitimate). The author argues that it is a crucial question which must be answered. He concludes that baier has not proven (...) that the normative criteria of justification involved in morality constitute a question for the philosopher. (wstaff). (shrink)

I. Professor William L. Rowe begins an interesting paper on the Cosmological Argument by stating that his ‘purpose …is not to resurrect it’ but ‘to uncover, clarify, and examine some of the philosophical concepts and theses essential to the reasoning exhibited in the argument’. However, in the concluding pages of his paper, Rowe is at some pains to show that his discussion does at least demonstrate that the Cosmological Argument is beyond the reach of criticisms levelled against it in the (...) works of its classical critics, Hume and Kant and their modern-day counterparts. To quote his concluding remark: ‘Like most important philosophical arguments, it appears that the Cosmological Argument is neither as good as its supporters have claimed it to be nor as bad as its critics have believed.’ Now I have long suspected that some such estimate of the Cosmological Argument was correct; however I do not think that Rowe's discussions in his paper establish his contention that the reports of the death of the Cosmological Argument have been premature. Nevertheless, Rowe's uncovering of the reasoning that lies behind the argument does have the merit of laying bare the precise point from which, as well as the direction in which, the defence of the argument should proceed if we are to truly make some headway on this hoary topic. In what follows, I will first try to show why I think Rowe's discussion fails to establish his conclusion and thereafter try to give the outline of a more successful strategy for arriving at the same conclusion. (shrink)

We present an axiomatization for Basic Propositional Calculus BPC and give a completeness theorem for the class of transitive Kripke structures. We present several refinements, including a completeness theorem for irreflexive trees. The class of intermediate logics includes two maximal nodes, one being Classical Propositional Calculus CPC, the other being E1, a theory axiomatized by T → ⊥. The intersection CPC ∩ E1 is axiomatizable by the Principle of the Excluded Middle A V ∨ ⌝A. If B is a formula (...) such that → B is not derivable, then the lattice of formulas built from one propositional variable p using only the binary connectives, is isomorphically preserved if B is substituted for p. A formula → B is derivable exactly when B is provably equivalent to a formula of the form → A) →. (shrink)

A bounded monotone sequence of reals without a limit is called a Specker sequence. In Russian constructive analysis, Church's Thesis permits the existence of a Specker sequence. In intuitionistic mathematics, Brouwer's Continuity Principle implies it is false that every bounded monotone sequence of real numbers has a limit. We claim that the existence of Specker sequences crucially depends on the properties of intuitionistic decidable sets. We propose a schema about intuitionistic decidability that asserts “there exists an intuitionistic enumerable set that (...) is not intuitionistic decidable” and show that the existence of a Specker sequence is equivalent to ED. We show that ED is consistent with some certain well known axioms of intuitionistic analysis as Weak Continuity Principle, bar induction, and Kripke Schema. Thus, the assumption of the existence of a Specker sequence is conceivable in intuitionistic analysis. We will also introduce the notion of double Specker sequence and study the existence of them. (shrink)

We prove that every infinite rooted narrow tree Kripke model of HA is locally PA.

Kolmogorov established the principle of the double negation translation by which to embed Classical Predicate Logic |${\operatorname {CQC}}$| into Intuitionistic Predicate Logic |${\operatorname {IQC}}$|⁠. We show that the obvious generalizations to the Basic Predicate Logic of [3] and to |${\operatorname {BQC}}$| of [12], a proper subsystem of |${\operatorname {IQC}}$|⁠, go through as well. The obvious generalizations of Kuroda’s embedding are shown to be equivalent to the Kolmogorov variant. In our proofs novel nontrivial techniques are needed to overcome the absence of (...) full modus ponens in Basic Predicate Logic. In [3] we argued that |${\operatorname {IQC}}$| is not the logic of constructive mathematics. Our doubts were far from new. New was that we put forward an alternative, |${\operatorname {BQC}}$|⁠. One concern is that |${\operatorname {BQC}}$| is too weak for serious mathematics, or even trivial. This paper is one step to alleviate such concerns. (shrink)

For the Heyting Arithmetic HA, $HA^{\text{*}} $ is defined [14, 15] as the theory $\left\{ {A|HA \vdash A^\square } \right\}$, where $A^\square $ is called the box translation of A. We characterize the ${\text{\Sigma }}_1 $-provability logic of $HA^{\text{*}} $ as a modal theory $iH_\sigma ^{\text{*}} $.

My attention in this paper will be focused almost exclusively on the interpretation of Part III of Hume's Dialogues Concerning Natural Religion suggested by Professor Nelson Pike at the very close of his excellent recent commentary on that enduring classic. 1 As I will show briefly in Section II below, Pike's interpretation of Part III emerges from the wider context of his quarrel with Kemp Smith in regard to the final outcome of these Dialogues . I find much in Pike's (...) commentary to applaud and to agree with, especially in its earlier sections, but on this whole question of Hume's final position in the Dialogues , I find his views less than convincing. But in this paper I will confine myself to showing what I think is wrong with his reading of Part III, and no more. 2 In particular, I will make no effort to challenge Pike's disagreement with Kemp Smith in regard to the final dialogue. Though Pike himself regards Part III as crucial, I am well aware that to make anything like a successful case against the kind of interpretation he favours of the upshot of the Dialogues much more would have to be done than I attempt in this paper. I submit this attempt, then, in partial fulfillment of a larger task to be completed at some future time. (shrink)

Let A be a subset of the constructive real line. What are the necessary and sufficient conditions for the set A such that A is continuously separated from other reals, i.e., there exists a continuous function f with f−1(0) = A? In this paper, we study the notions of closed sets and closure maps in constructive reverse mathematics.

Few people would care to deny, whether within India or without, that Buddha is the greatest Indian of all times. Whether from the standpoint of the purity of his life, the daring originality and novelty of his thought, or the extent of his influence in shaping the culture of the world, it would be hard to beat the record of Buddha. Even making every allowance for the common idea that no man is a prophet in his own land, it is (...) difficult to believe that for the last thousand years Buddha has been practically an exile from the land of his birth. It is nothing short of an irony of history, and nothing short of a tragedy for India, that the great unifying force that he represented in his time and does represent even to-day has been allowed to run waste and the great moral stamina that he sought to supply failed in its historic mission. (shrink)

A latarre is a lattice with an arrow. Its axiomatization looks natural. Latarres have a nontrivial theory which permits many constructions of latarres. Latarres appear as an end result of a series of generalizations of better known structures. These include Boolean algebras and Heyting algebras. Latarres need not have a distributive lattice.

We represent the well-known surprise exam paradox in constructive and computable mathematics and offer solutions. One solution is based on Brouwer’s continuity principle in constructive mathematics, and the other involves type 2 Turing computability in classical mathematics. We also discuss the backward induction paradox for extensive form games in constructive logic.

Let denote a first‐order logic in a language that contains infinitely many constant symbols and also containing intuitionistic logic. By, we mean the associated logic axiomatized by the double negation of the universal closure of the axioms of plus. We shall show that if is strongly complete for a class of Kripke models, then is strongly complete for the class of Kripke models that are ultimately in.

We prove that Basic Arithmetic, BA, has the de Jongh property, i.e., for any propositional formula A(p 1,..., p n ) built up of atoms p 1,..., p n, BPC $${\vdash}$$ A(p 1,..., p n ) if and only if for all arithmetical sentences B 1,..., B n, BA $${\vdash}$$ A(B 1,..., B n ). The technique used in our proof can easily be applied to some known extensions of BA.

Avicenna introduces the primary propositions as the most fundamental principles of knowledge. However, as far as we are aware, Avicenna’s primaries have not yet been independently studied. Nor do Avicenna scholars agree on how to characterize them in the language of contemporary philosophy. It is well-known that the primaries are indemonstrable; nonetheless, it is not clear what the genealogy of the primaries is, how, epistemologically speaking, they can be distinguished from other principles, what their phenomenology is, what the cause of (...) the assent to them is, how to explain the relationship between the ‘innate [nature] of the intellect’ and the primaries and, finally, back to their indemonstrability, in what sense they are ‘indemonstrable’. We will try to fill this gap. As a corollary, we will explain why Gutas’s view [Gutas, Dimitri.... (shrink)

MY PAPER EXAMINES THE ’VIOLATION’ CONCEPT OF THE MIRACULOUS, INVOLVING THE OCCURRENCE OF AN EVENT RULED OUT BY A LAW OF NATURE. ANY BELIEF IN THE OCCURRENCE OF SUCH AN EVENT IS IRRATIONAL, IN THE SENSE IN WHICH IT WOULD BE IRRATIONAL FOR YOU TO BELIEVE AT THIS MOMENT THAT YOU WERE NOT READING THIS ABSTRACT BUT WERE HALLUCINATING. TO SHOW THAT IT IS NOT ALWAYS IRRATIONAL TO BELIEVE IN MIRACLES, ONE MUST ASSERT THAT TO KNOW WITH CERTAINTY THAT AN (...) EVENT IS PHYSICALLY IMPOSSIBLE, IS NOT TO KNOW WITH CERTAINTY THAT IT IS IMPOSSIBLE, ON GROUNDS THAT ITS OCCURRENCE DOES NOT INVOLVE A SELF-CONTRADICTION. BUT SUCH A PREMISE LEADS TO A FORM OF GENERAL SKEPTICISM WHICH WOULD MAKE IT IMPOSSIBLE EVER TO ESTABLISH THAT ANY EVENT HAD OCCURRED. (shrink)

We introduce two Gentzen-style sequent calculus axiomatizations for conservative extensions of basic propositional logic. Our first axiomatization is an ipmrovement of, in the sense that it has a kind of the subformula property and is a slight modification of. In this system the cut rule is eliminated. The second axiomatization is a classical conservative extension of basic propositional logic. Using these axiomatizations, we prove interpolation theorems for basic propositional logic.

Basic Predicate Logic, BQC, is a proper subsystem of Intuitionistic Predicate Logic, IQC. For every formula in the language {, , , , , , }, we associate two sequences of formulas 0,1,... and 0,1,... in the same language. We prove that for every sequent , there are natural numbers m, n, such that IQC , iff BQC n m. Some applications of this translation are mentioned.

We study Basic Arithmetic, $$\textsf{BA}$$ introduced by Ruitenburg (Notre Dame J Formal Logic 39:18–46, 1998). $$\textsf{BA}$$ is an arithmetical theory based on basic logic which is weaker than intuitionistic logic. We show that the class of the provably total recursive functions of $$\textsf{BA}$$ is a proper sub-class of the primitive recursive functions. Three extensions of $$\textsf{BA}$$, called $$\textsf{BA}+\mathsf U$$, $$\mathsf {BA_{\mathrm c}}$$ and $$\textsf{EBA}$$ are investigated with relation to their provably total recursive functions. It is shown that the provably total (...) recursive functions of these three extensions of $$\textsf{BA}$$ are exactly the primitive recursive functions. Moreover, among other things, it is shown that the well-known MRDP theorem does not hold in $$\textsf{BA}$$, $$\textsf{BA}+\mathsf U$$, $$\mathsf {BA_{\mathrm c}}$$, but holds in $$\textsf{EBA}$$. (shrink)

We present axiom systems, and provide soundness and strong completeness theorems, for classes of Kripke models with restricted extension rules among the node structures of the model. As examples we present an axiom system for the class of cofinal extension Kripke models, and an axiom system for the class of end-extension Kripke models. We also show that Heyting arithmetic is strongly complete for its class of end-extension models. Cofinal extension models of HA are models of Peano arithmetic.

We generalize the double negation construction of Boolean algebras in Heyting algebras to a double negation construction of the same in Visser algebras. This result allows us to generalize Glivenko’s theorem from intuitionistic propositional logic and Heyting algebras to Visser’s basic propositional logic and Visser algebras.

In this paper we prove a bounded translation of intuitionistic propositional logic into basic propositional logic. Our new theorem, compared with the translation theorem in [1], has the advantage that it gives an effective bound on the translation, depending on the complexity of formulas.